00100 VAR:x,y,z,s; 00120 PRE_OP:cup,tbl,tat,thd,any,letgo, go ,pu,0,s0,fork; 00160 INF_PRED:=; EQUALITY: =; 00170 INF_OP:∩,∪; 00180 00400 ((x ∪ y)∩ z = 0) ⊃((x ∩ z) = 0 ∧ (y ∩ z = 0)); 00500 FRED: 00550 tat(x,go(x,s))=tat(x,s) ∪ thd(s); 00600 thd(pu(go(x,s)))=any(tat(x,go(x,s))); 00700 thd(letgo(s))=0; 00800 any(tat(cup,s0))∩fork=0; 00850 THEOREM:∃s¬ tat(tbl,s)∩ fork =0; 00900 ;